H-Termination proof of /home/matraf/haskell/eval_FullyBlown

YES 0.584 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/List.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:

↳ HASKELL

  ↳ CR

mainModule List

((insert :: () -> [()] -> [()]) :: () -> [()] -> [()])

module List where

import qualified Maybe
import qualified Prelude

insert :: Ord a => a -> [a] -> [a]

insert

e ls

insertBy compare e ls

insertBy :: (a -> a -> Ordering) -> a -> [a] -> [a]

insertBy

_ x []

x : []

insertBy

cmp x ys@(y : ys')

case	cmp x y of
	GT	->	y : insertBy cmp x ys'
	_	->	x : ys

module Maybe where

import qualified List
import qualified Prelude

Case Reductions:
The following Case expression

case cmp x y of
GT → y : insertBy cmp x ys'

_ → x : ys

is transformed to

insertBy0 y cmp x ys' ys GT = y : insertBy cmp x ys'

insertBy0 y cmp x ys' ys _ = x : ys

↳ HASKELL

  ↳ CR

    ↳ HASKELL

      ↳ BR

mainModule List

((insert :: () -> [()] -> [()]) :: () -> [()] -> [()])

module List where

import qualified Maybe
import qualified Prelude

insert :: Ord a => a -> [a] -> [a]

insert

e ls

insertBy compare e ls

insertBy :: (a -> a -> Ordering) -> a -> [a] -> [a]

insertBy	_ x []	=	x : []
insertBy	cmp x ys@(y : ys')	=	insertBy0 y cmp x ys' ys (cmp x y)

insertBy0	y cmp x ys' ys GT	=	y : insertBy cmp x ys'
insertBy0	y cmp x ys' ys _	=	x : ys

module Maybe where

import qualified List
import qualified Prelude

Replaced joker patterns by fresh variables and removed binding patterns.
Binding Reductions:
The bind variable of the following binding Pattern

ys@(vy : vz)

is replaced by the following term

vy : vz

↳ HASKELL

  ↳ CR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

mainModule List

((insert :: () -> [()] -> [()]) :: () -> [()] -> [()])

module List where

import qualified Maybe
import qualified Prelude

insert :: Ord a => a -> [a] -> [a]

insert

e ls

insertBy compare e ls

insertBy :: (a -> a -> Ordering) -> a -> [a] -> [a]

insertBy	vx x []	=	x : []
insertBy	cmp x (vy : vz)	=	insertBy0 vy cmp x vz (vy : vz) (cmp x vy)

insertBy0	y cmp x ys' ys GT	=	y : insertBy cmp x ys'
insertBy0	y cmp x ys' ys vw	=	x : ys

module Maybe where

import qualified List
import qualified Prelude

Cond Reductions:
The following Function with conditions

undefined

| False

= undefined

is transformed to

undefined = undefined1

undefined0 True = undefined

undefined1 = undefined0 False

↳ HASKELL

  ↳ CR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

mainModule List

(insert :: () -> [()] -> [()])

module List where

import qualified Maybe
import qualified Prelude

insert :: Ord a => a -> [a] -> [a]

insert

e ls

insertBy compare e ls

insertBy :: (a -> a -> Ordering) -> a -> [a] -> [a]

insertBy	vx x []	=	x : []
insertBy	cmp x (vy : vz)	=	insertBy0 vy cmp x vz (vy : vz) (cmp x vy)

insertBy0	y cmp x ys' ys GT	=	y : insertBy cmp x ys'
insertBy0	y cmp x ys' ys vw	=	x : ys

module Maybe where

import qualified List
import qualified Prelude

Haskell To QDPs

digraph dp_graph {
node [outthreshold=100, inthreshold=100];1[label="insert",fontsize=16,color="grey",shape="box"];1 -> 3[label="",style="dashed", color="grey", weight=3];
3[label="insert ww3",fontsize=16,color="grey",shape="box"];3 -> 4[label="",style="dashed", color="grey", weight=3];
4[label="insert ww3 ww4",fontsize=16,color="black",shape="triangle"];4 -> 5[label="",style="solid", color="black", weight=3];
5[label="insertBy compare ww3 ww4",fontsize=16,color="burlywood",shape="box"];14[label="ww4/ww40 : ww41",fontsize=10,color="white",style="solid",shape="box"];5 -> 14[label="",style="solid", color="burlywood", weight=9];
14 -> 6[label="",style="solid", color="burlywood", weight=3];
15[label="ww4/[]",fontsize=10,color="white",style="solid",shape="box"];5 -> 15[label="",style="solid", color="burlywood", weight=9];
15 -> 7[label="",style="solid", color="burlywood", weight=3];
6[label="insertBy compare ww3 (ww40 : ww41)",fontsize=16,color="black",shape="box"];6 -> 8[label="",style="solid", color="black", weight=3];
7[label="insertBy compare ww3 []",fontsize=16,color="black",shape="box"];7 -> 9[label="",style="solid", color="black", weight=3];
8[label="insertBy0 ww40 compare ww3 ww41 (ww40 : ww41) (compare ww3 ww40)",fontsize=16,color="burlywood",shape="box"];16[label="ww3/()",fontsize=10,color="white",style="solid",shape="box"];8 -> 16[label="",style="solid", color="burlywood", weight=9];
16 -> 10[label="",style="solid", color="burlywood", weight=3];
9[label="ww3 : []",fontsize=16,color="green",shape="box"];10[label="insertBy0 ww40 compare () ww41 (ww40 : ww41) (compare () ww40)",fontsize=16,color="burlywood",shape="box"];17[label="ww40/()",fontsize=10,color="white",style="solid",shape="box"];10 -> 17[label="",style="solid", color="burlywood", weight=9];
17 -> 11[label="",style="solid", color="burlywood", weight=3];
11[label="insertBy0 () compare () ww41 (() : ww41) (compare () ())",fontsize=16,color="black",shape="box"];11 -> 12[label="",style="solid", color="black", weight=3];
12[label="insertBy0 () compare () ww41 (() : ww41) EQ",fontsize=16,color="black",shape="box"];12 -> 13[label="",style="solid", color="black", weight=3];
13[label="() : () : ww41",fontsize=16,color="green",shape="box"];}

insertBy0	y cmp x ys' ys GT	= y : insertBy cmp x ys'
insertBy0	y cmp x ys' ys _	= x : ys